T:Type, L:(T List), x, y:T.
no_repeats(T;L)  adjacent(T;L;x;y)  (z:T. x before z  L  (y before z  L  (z = y))) 

latex

Definitions	s = t, P  Q, Type, left + right, type List, False, x:AB(x), P  Q, x:A. B(x), A, no_repeats(T;l), adjacent(T;L;x;y), x:A  B(x), x:A. B(x), L1  L2, x before y  l, a < b, (x  l), Dec(P), P & Q, P  Q, , A  B, Atom, {i..j}, , b, x,y:A//B(x;y), b | a, a ~ b, |p|, a  b, a <p b, |g|, a < b, A c B, f(a), x f y, |r|, xL. P(x), (xL.P(x)), Unit, {T}, Void, t  T
Lemmas	no repeats iff, l before antisymmetry, before-adjacent, no repeats wf, adjacent wf, adjacent-member, l before member, l tricotomy, l before wf